1. Field of the Invention
The present invention relates generally to the field of embedded system verification, and more particularly, to a general methodology for worst-case and busy period analysis of systems having discrete observable signals.
2. Description of the Related Art
Embedded systems are becoming more complex, and controlling ever more critical processes. It is thus not surprising that significant research efforts have emerged for developing methodologies to efficiently design such systems. Because the various embedded environments often impose strict limitations, verification of embedded systems must not be limited to their functionality, but must also include constraints such as timing performance, and power consumption.
Embedded system verification is difficult, especially for software code, because system responses need to be checked for all legal behaviors of the environment. Typically, there are infinitely many such behaviors. Even when the problem is reduced by formal reasoning to enumerating finitely many internal system states, the number of such states is usually still computationally prohibitive. Using abstractions and implicit state enumeration can simplify the problem, but complete formal verification is at best at the performance limit of existing computers (and often far beyond).
Presently, the most widely used approach to verification of embedded systems is simulation. This approach has an obvious weakness in that only a few of the infinitely many input patterns can be tried, and thus complete verification can never be guaranteed. An alternative approach is the worst-case analysis methodology, where the system response is analyzed only for those behaviors of the environment that are the hardest for the system to execute. Worst-case analysis is a well known engineering method, but so far it has been used ad-hoc, with separate techniques for specific system properties. Furthermore, there is currently no systematic methodology for performing worst-case analysis of software.
Another technique that is used is prototyping. In prototyping, a physical model of a system is built consisting typically of a chosen microprocessor (or micro-controller), memory and some interface circuitry. The prototype is then exercised with some set of input sequences, and the outputs of the system are monitored for correctness. Both simulation and prototyping have the common problem that there are infinitely many possible input sequences, so even if a system behaves correctly for all sequences in the test set, there still is no guarantee that the system will behave correctly for a different input sequence. In other words, using these prior methods, it can be shown that a system does not meet a given constraint, but it can never be proven that the system does in fact meet the constraint.
Busy-period analysis can be expressed as a standard verification problem in a formalism that combines timing information with finite-state systems. For example, Balarin B et.al., Formal Verification of the PATHO real-time operating system, Proceedings of the 33rd Conference on Decision and Control, CDC ""94, December 1994, herein incorporated by reference, formulated this problem as a reachability problem for timed automata. Choi et.al., The Specification and Schedulability Analysis of Real-Time Systems Using ACSR, Proceedings of EEEE Real-Time Systems Symposium, pages 266-275, EEE Computer Society Press, December 1995, herein incorporated by reference, formulated the problem as an equivalence checking problem in a process algebra ACSR-VP. Both of these approaches have the advantage of being exact, but they both suffer from severe limitations due to the computational complexity involved. Thus, it is highly unlikely that these approaches could ever be applied to practical systems of realistic size.
There are also well established algorithms for timing analysis of combinational logic circuits, as disclosed in for example McGeer et al., Delay Models and Exact Timing Analysis, Logic Synthesis and Optimization, T. Sasao, editor, Kluwar Academic Publishers, 1993, herein incorporated by reference. Like reactive real-time systems, combinational logic circuits also consist of interacting components (gates), but unlike gates which can propagate the signals concurrently, only one software task can execute at a time on a given processor. This significant difference makes combinational logic circuits an unsuitable model for reactive real-time systems.
In a data-flow graph model, a system consists of actors, which take items of data from their inputs and produce items of data on their output. The actors can act only if data items are present on all of their inputs. This feature enables very predictable scheduling of actors (and thus simple timing analysis). It is now widely accepted that because of this feature, data-flow graphs are well suited to model data-intensive systems (e.g. those appearing in signal processing), but not well suited for reactive control-dominated systems where a reaction is required for many different conditions in the environment.
A variety of verification models have been considered over the past several decades by researchers in the real-time systems community. Most of the models are extensions or modifications of the one introduced by Liu and Layland, Scheduling Algorithms for Multiprogramming in a Hard-Realtime Environment, Journal of the Association for Computing Machinery, 20(1):46-61, January 1973, herein incorporated by reference. These models have considered systems in which all the tasks are independent (i.e. no precedence or exclusion constraints), periodic, and occurring for the first time at time zero.
The restrictions on this model have been somewhat relaxed by later researchers, although several significant limitations are still present in all the previous approaches:
The processing time requirements of a component is assumed to be constant.
An execution of a component is assumed to cause executions of all of its successors, while in reality a component may be enabling only some successors, depending on the inputs and internal states.
Previous approaches are restricted to acyclic system graphs, i.e. to systems for which there exists a well defined unidirectional information flow.
Previous approaches are applicable only to systems with static priority scheduling.
Therefore, there is a need for an improved procedure for verification of embedded systems.
The present invention is a general methodology for worst-case and busy period analysis of systems with discrete observable signals. Most embedded systems, as well as many others, fit into this category. The methodology can be used to verify different properties of systems such as power consumption, timing performance, or resource utilization. The busy period analysis determines the maximum length of time a processor can be busy. The present methods are conservative, i.e. the system is guaranteed to perform within the bounds computed by the methodology, but these bounds are not necessarily the best possible.
According to this first embodiment of the present method, a signature "sgr" is chosen and a "sgr"-abstraction F is created, based on the system and the particular property to be analyzed. This procedure requires a user to facilitate the creation of an appropriate signature and "sgr"-abstraction. Next, for a given length of time T, a worst-case signature s is determined. From the signature s the worst-case boundary conditions are determined.
The present invention may also be applied to timing analysis of embedded systems implemented on a single processor. Timing analysis of embedded software system can be divided into two sub-problems: local and global. The local sub-problem is to determine processing time requirements for a piece of code implementing a single component of the system. The global sub-problem is to determine response time of the system given processing time requirements of system components and taking into account that response to some requests may be delayed by responses to other requests. The present invention addresses only the global sub-problem and assumes that a solution to the local sub-problem is available.
The procedure calculates a time T which is an upper bound on the time a processor can be busy (i.e. busy period). Thus, for the busy-period analysis, the time T is no longer fixed. As in the first embodiment, a signature "sgr" is selected and a "sgr"-abstraction F is created. A workload function R is chosen, and a signature s and time T are calculated. The calculated time T is an upper bound on the length of a busy period for the given system.